3.11.1 Language Reference

3.11.1 Language Reference

In this section, we present modeling languages which are expressive enough to capture all core features of Web Service choreography and orchestration. There are two reasons for introducing intermediate modeling languages for Web Services. First, heavy languages like WS-CDL or WS-BPEL are designed for machine consumption and therefore are lengthy and complicated in structure. Moreover, there are mismatches between WS-CDL and WS-BPEL. For instance, WS-CDL allows channel passing whereas WS-BPEL does not. The intermediate languages focus on the interactive behavioral aspect. We develop parsers, compilers as well as formal operational semantics for the intermediate languages so that users can quickly write a Web service model and analyze it, using our visualized simulator, verifier and synthesizer. The languages are developed based on previous work of formal models for WS-CDL and WS-BPEL. They cover all main features like synchronous/asynchronous message passing, channel passing, process forking, parallel composition, shared variables, etc.. In addition, based on the intermediate languages and their semantic models (namely, labeled transition systems), our verification and synthesis approaches are not bound to one particular Web service language. This is important because Web Service languages evolves rapidly. Being based on intermediate languages gives us opportunity to quickly cope with new syntaxes or features (e.g., by tuning the preprocessing component).

The language syntax structures are listed as follows. The complete grammar rules can be found in Section 3.11.1.5. In Web Service module, we assume each model can have maximum one choreography and orchestration.

3.11.1.1 Global Definitions

3.11.1.2 Web Service Choreography

3.11.1.3 Web Service Orchestration

3.11.1.4 Assertions